T:Type, P1, P2:(T), L:(T List). filter(P1;filter(P2;L)) ~ filter(P2;filter(P1;L)) 

latex

ProofTree

Definitions	t  T, type List, x:AB(x), s ~ t, x:A. B(x), , Type, b, A, b, s = t, , f(a), P  Q, x:A  B(x), P & Q, P  Q, Unit, left + right, {T}, SQType(T)
Lemmas	not assert elim, bool sq, assert elim, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bnot wf, not wf, assert wf, bool wf